$\forall$$M$:MsgA, $k$:Knd, $x$:Id. $M$:$k$ may not read $x$ $\Leftrightarrow$ $\neg$$M$.rframe($k$ reads $x$)